Termination proof of /tmp/tmpXUZ5bQ/ExIntrod

Termination of the following Term Rewriting System could not be shown:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The replacement map contains the following entries:

fact: {1}
if: {1}
zero: {1}
s: {1}
0: empty set
prod: {1, 2}
p: {1}
add: {1, 2}
true: empty set
false: empty set

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The replacement map contains the following entries:

fact: {1}
if: {1}
zero: {1}
s: {1}
0: empty set
prod: {1, 2}
p: {1}
add: {1, 2}
true: empty set
false: empty set

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The replacement map contains the following entries:

fact: {1}
if: {1}
zero: {1}
s: {1}
0: empty set
prod: {1, 2}
p: {1}
add: {1, 2}
true: empty set
false: empty set

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {fact, zero, s, prod, p, add, FACT, ZERO, ADD, PROD, P} are replacing on all positions.
For all symbols f in {if, IF} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

FACT(X) → IF(zero(X), s(0), prod(X, fact(p(X))))
FACT(X) → ZERO(X)
ADD(s(X), Y) → ADD(X, Y)
PROD(s(X), Y) → ADD(Y, prod(X, Y))
PROD(s(X), Y) → PROD(X, Y)

The collapsing dependency pairs are DP_c:

IF(true, X, Y) → X
IF(false, X, Y) → Y

The hidden terms of R are:

prod(X, fact(p(X)))
fact(p(X))
p(X)

Every hiding context is built from:

p on positions {1}
fact on positions {1}
prod on positions {1, 2}

Hence, the new unhiding pairs DP_u are :

IF(true, X, Y) → U(X)
IF(false, X, Y) → U(Y)
U(p(x_0)) → U(x_0)
U(fact(x_0)) → U(x_0)
U(prod(x_0, x_1)) → U(x_0)
U(prod(x_0, x_1)) → U(x_1)
U(prod(X, fact(p(X)))) → PROD(X, fact(p(X)))
U(fact(p(X))) → FACT(p(X))
U(p(X)) → P(X)

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 4 less nodes.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

              ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {fact, zero, s, prod, p, add, ADD} are replacing on all positions.
For all symbols f in {if} we have µ(f) = {1}.

The TRS P consists of the following rules:

ADD(s(X), Y) → ADD(X, Y)

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

ADD(s(X), Y) → ADD(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
ADD(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

              ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {fact, zero, s, prod, p, add} are replacing on all positions.
For all symbols f in {if} we have µ(f) = {1}.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {fact, zero, s, prod, p, add, PROD} are replacing on all positions.
For all symbols f in {if} we have µ(f) = {1}.

The TRS P consists of the following rules:

PROD(s(X), Y) → PROD(X, Y)

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

PROD(s(X), Y) → PROD(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
PROD(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPNarrowingProcessor

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {fact, zero, s, prod, p, add, FACT} are replacing on all positions.
For all symbols f in {if, IF} we have µ(f) = {1}.
The symbols in {U} are not replacing on any position.

The TRS P consists of the following rules:

IF(true, X, Y) → U(X)
U(p(x_0)) → U(x_0)
U(fact(x_0)) → U(x_0)
U(prod(x_0, x_1)) → U(x_0)
U(prod(x_0, x_1)) → U(x_1)
U(fact(p(X))) → FACT(p(X))
FACT(X) → IF(zero(X), s(0), prod(X, fact(p(X))))
IF(false, X, Y) → U(Y)

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

Using the Context-Sensitive Narrowing Processor
the pair FACT(X) → IF(zero(X), s(0), prod(X, fact(p(X))))
was transformed to the following new pairs:

FACT(0) → IF(true, s(0), prod(0, fact(p(0))))
FACT(s(x0)) → IF(false, s(0), prod(s(x0), fact(p(s(x0)))))

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPNarrowingProcessor

                  ↳ QCSDP

                    ↳ ConvertedToQDPProblemProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

IF(false, X, Y) → U(Y)
FACT(s(x0)) → IF(false, s(0), prod(s(x0), fact(p(s(x0)))))
U(p(x_0)) → U(x_0)
U(fact(p(X))) → FACT(p(X))
U(prod(x_0, x_1)) → U(x_0)
U(prod(x_0, x_1)) → U(x_1)
IF(true, X, Y) → U(X)
U(fact(x_0)) → U(x_0)
FACT(0) → IF(true, s(0), prod(0, fact(p(0))))

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

Converted QDP Problem, but could not keep Q or minimality.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPNarrowingProcessor

                  ↳ QCSDP

                    ↳ ConvertedToQDPProblemProof

                      ↳ QDP

                        ↳ Narrowing

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

IF(false, X, Y) → U(Y)
FACT(s(x0)) → IF(false, s(0), prod(s(x0), fact(p(s(x0)))))
U(p(x_0)) → U(x_0)
U(fact(p(X))) → FACT(p(X))
U(prod(x_0, x_1)) → U(x_0)
U(prod(x_0, x_1)) → U(x_1)
U(fact(x_0)) → U(x_0)
IF(true, X, Y) → U(X)
FACT(0) → IF(true, s(0), prod(0, fact(p(0))))

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

Q is empty.
We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U(fact(p(X))) → FACT(p(X)) at position [0] we obtained the following new rules:

U(fact(p(s(x0)))) → FACT(x0)

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPNarrowingProcessor

                  ↳ QCSDP

                    ↳ ConvertedToQDPProblemProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

IF(false, X, Y) → U(Y)
FACT(s(x0)) → IF(false, s(0), prod(s(x0), fact(p(s(x0)))))
U(p(x_0)) → U(x_0)
U(fact(p(s(x0)))) → FACT(x0)
U(prod(x_0, x_1)) → U(x_0)
U(prod(x_0, x_1)) → U(x_1)
IF(true, X, Y) → U(X)
U(fact(x_0)) → U(x_0)
FACT(0) → IF(true, s(0), prod(0, fact(p(0))))

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

Q is empty.
We have to consider all (P,Q,R)-chains.
We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(zero(x1)) → ZEROACTIVE(mark(x1))
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(x1, x2)) → ADDACTIVE(mark(x1), mark(x2))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → ZEROACTIVE(mark(X))
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(x1, x2)) → PRODACTIVE(mark(x1), mark(x2))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(zero(x1)) → ZEROACTIVE(mark(x1))
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(x1, x2)) → ADDACTIVE(mark(x1), mark(x2))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → ZEROACTIVE(mark(X))
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(x1, x2)) → PRODACTIVE(mark(x1), mark(x2))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(x1, x2)) → ADDACTIVE(mark(x1), mark(x2))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(x1, x2)) → PRODACTIVE(mark(x1), mark(x2))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(add(x1, x2)) → ADDACTIVE(mark(x1), mark(x2)) at position [0] we obtained the following new rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(add(true, y1)) → ADDACTIVE(true, mark(y1))
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(add(false, y1)) → ADDACTIVE(false, mark(y1))
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(add(true, y1)) → ADDACTIVE(true, mark(y1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(x1, x2)) → PRODACTIVE(mark(x1), mark(x2))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(add(false, y1)) → ADDACTIVE(false, mark(y1))
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(x1, x2)) → PRODACTIVE(mark(x1), mark(x2))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(prod(x1, x2)) → PRODACTIVE(mark(x1), mark(x2)) at position [0] we obtained the following new rules:

MARK(prod(false, y1)) → PRODACTIVE(false, mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(true, y1)) → PRODACTIVE(true, mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(0, y1)) → PRODACTIVE(0, mark(y1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(true, y1)) → PRODACTIVE(true, mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(false, y1)) → PRODACTIVE(false, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(0, y1)) → PRODACTIVE(0, mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3)
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(if(x1, x2, x3)) → IFACTIVE(mark(x1), x2, x3) at position [0] we obtained the following new rules:

MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(if(0, y1, y2)) → IFACTIVE(0, y1, y2)
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
MARK(if(s(x0), y1, y2)) → IFACTIVE(s(mark(x0)), y1, y2)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(x1)) → PACTIVE(mark(x1))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(if(0, y1, y2)) → IFACTIVE(0, y1, y2)
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(if(s(x0), y1, y2)) → IFACTIVE(s(mark(x0)), y1, y2)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
PRODACTIVE(s(X), Y) → MARK(X)
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(prod(x1, x2)) → MARK(x1)
MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
PRODACTIVE(s(X), Y) → MARK(X)
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(x1)) → PACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(p(x1)) → PACTIVE(mark(x1)) at position [0] we obtained the following new rules:

MARK(p(true)) → PACTIVE(true)
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(false)) → PACTIVE(false)
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(p(0)) → PACTIVE(0)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(false)) → PACTIVE(false)
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(p(true)) → PACTIVE(true)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
PRODACTIVE(s(X), Y) → MARK(X)
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(0)) → PACTIVE(0)
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
PRODACTIVE(s(X), Y) → MARK(X)
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ADDACTIVE(s(X), Y) → ADDACTIVE(mark(X), mark(Y)) at position [0] we obtained the following new rules:

ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(zero(x0)), y1) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(true), y1) → ADDACTIVE(true, mark(y1))
ADDACTIVE(s(false), y1) → ADDACTIVE(false, mark(y1))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(true), y1) → ADDACTIVE(true, mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(zero(x0)), y1) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
ADDACTIVE(s(false), y1) → ADDACTIVE(false, mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ Narrowing

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
ADDACTIVE(s(zero(x0)), y1) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule PRODACTIVE(s(X), Y) → PRODACTIVE(mark(X), mark(Y)) at position [0] we obtained the following new rules:

PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(true), y1) → PRODACTIVE(true, mark(y1))
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
PRODACTIVE(s(0), y1) → PRODACTIVE(0, mark(y1))
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(false), y1) → PRODACTIVE(false, mark(y1))
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(fact(x1)) → MARK(x1)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(zero(x0)), y1) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
PRODACTIVE(s(false), y1) → PRODACTIVE(false, mark(y1))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(true), y1) → PRODACTIVE(true, mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(0), y1) → PRODACTIVE(0, mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 3 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
ADDACTIVE(s(zero(x0)), y1) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

ADDACTIVE(s(zero(x0)), y1) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(add(zero(x0), y1)) → ADDACTIVE(zeroActive(mark(x0)), mark(y1))

The remaining pairs can at least be oriented weakly.

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
PACTIVE(s(X)) → MARK(X)
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ADDACTIVE(x₁, x₂)) = x₁
POL(FACTACTIVE(x₁)) = 1
POL(IFACTIVE(x₁, x₂, x₃)) = 1
POL(MARK(x₁)) = 1
POL(PACTIVE(x₁)) = 1
POL(PRODACTIVE(x₁, x₂)) = 1
POL(add(x₁, x₂)) = 0
POL(addActive(x₁, x₂)) = x₁
POL(fact(x₁)) = 1
POL(factActive(x₁)) = 1
POL(false) = 0
POL(if(x₁, x₂, x₃)) = 0
POL(ifActive(x₁, x₂, x₃)) = 1
POL(mark(x₁)) = 1
POL(p(x₁)) = 0
POL(pActive(x₁)) = x₁
POL(prod(x₁, x₂)) = 0
POL(prodActive(x₁, x₂)) = 1
POL(s(x₁)) = 1
POL(true) = 0
POL(zero(x₁)) = 0
POL(zeroActive(x₁)) = 0

The following usable rules [17] were oriented:

zeroActive(s(X)) → false
zeroActive(0) → true
prodActive(x1, x2) → prod(x1, x2)
addActive(x1, x2) → add(x1, x2)
factActive(x1) → fact(x1)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
ifActive(true, X, Y) → mark(X)
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(0, X) → mark(X)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
mark(fact(x1)) → factActive(mark(x1))
mark(p(x1)) → pActive(mark(x1))
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
pActive(s(X)) → mark(X)
ifActive(false, X, Y) → mark(Y)
mark(true) → true
mark(false) → false
mark(s(x1)) → s(mark(x1))
mark(0) → 0
pActive(x1) → p(x1)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
ifActive(x1, x2, x3) → if(x1, x2, x3)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ QDPOrderProof

                                                                ↳ QDP

                                                                  ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(p(zero(x0))) → PACTIVE(zeroActive(mark(x0)))

The remaining pairs can at least be oriented weakly.

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
IFACTIVE(false, X, Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ADDACTIVE(x₁, x₂)) = 1
POL(FACTACTIVE(x₁)) = 1
POL(IFACTIVE(x₁, x₂, x₃)) = 1
POL(MARK(x₁)) = 1
POL(PACTIVE(x₁)) = x₁
POL(PRODACTIVE(x₁, x₂)) = 1
POL(add(x₁, x₂)) = 0
POL(addActive(x₁, x₂)) = x₁
POL(fact(x₁)) = 0
POL(factActive(x₁)) = 1
POL(false) = 0
POL(if(x₁, x₂, x₃)) = 1
POL(ifActive(x₁, x₂, x₃)) = 1
POL(mark(x₁)) = 1
POL(p(x₁)) = 0
POL(pActive(x₁)) = x₁
POL(prod(x₁, x₂)) = 0
POL(prodActive(x₁, x₂)) = 1
POL(s(x₁)) = 1
POL(true) = 0
POL(zero(x₁)) = 0
POL(zeroActive(x₁)) = 0

The following usable rules [17] were oriented:

zeroActive(s(X)) → false
zeroActive(0) → true
prodActive(x1, x2) → prod(x1, x2)
addActive(x1, x2) → add(x1, x2)
factActive(x1) → fact(x1)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
ifActive(true, X, Y) → mark(X)
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(0, X) → mark(X)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
mark(fact(x1)) → factActive(mark(x1))
mark(p(x1)) → pActive(mark(x1))
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
pActive(s(X)) → mark(X)
ifActive(false, X, Y) → mark(Y)
mark(true) → true
mark(false) → false
mark(s(x1)) → s(mark(x1))
mark(0) → 0
pActive(x1) → p(x1)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
ifActive(x1, x2, x3) → if(x1, x2, x3)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ QDPOrderProof

                                                                ↳ QDP

                                                                  ↳ QDPOrderProof

                                                                    ↳ QDP

                                                                      ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

PRODACTIVE(s(zero(x0)), y1) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))
MARK(prod(zero(x0), y1)) → PRODACTIVE(zeroActive(mark(x0)), mark(y1))

The remaining pairs can at least be oriented weakly.

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
FACTACTIVE(X) → MARK(X)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

Used ordering: Polynomial interpretation [25]:

POL(0) = 1
POL(ADDACTIVE(x₁, x₂)) = 1
POL(FACTACTIVE(x₁)) = 1
POL(IFACTIVE(x₁, x₂, x₃)) = 1
POL(MARK(x₁)) = 1
POL(PACTIVE(x₁)) = 1
POL(PRODACTIVE(x₁, x₂)) = x₁
POL(add(x₁, x₂)) = 0
POL(addActive(x₁, x₂)) = x₁
POL(fact(x₁)) = 0
POL(factActive(x₁)) = 1
POL(false) = 0
POL(if(x₁, x₂, x₃)) = 0
POL(ifActive(x₁, x₂, x₃)) = 1
POL(mark(x₁)) = 1
POL(p(x₁)) = 0
POL(pActive(x₁)) = x₁
POL(prod(x₁, x₂)) = 0
POL(prodActive(x₁, x₂)) = x₁
POL(s(x₁)) = 1
POL(true) = 0
POL(zero(x₁)) = 0
POL(zeroActive(x₁)) = 0

The following usable rules [17] were oriented:

zeroActive(s(X)) → false
zeroActive(0) → true
prodActive(x1, x2) → prod(x1, x2)
addActive(x1, x2) → add(x1, x2)
factActive(x1) → fact(x1)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
ifActive(true, X, Y) → mark(X)
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(0, X) → mark(X)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
mark(fact(x1)) → factActive(mark(x1))
mark(p(x1)) → pActive(mark(x1))
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
pActive(s(X)) → mark(X)
ifActive(false, X, Y) → mark(Y)
mark(true) → true
mark(false) → false
mark(s(x1)) → s(mark(x1))
mark(0) → 0
pActive(x1) → p(x1)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
ifActive(x1, x2, x3) → if(x1, x2, x3)

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ Narrowing

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ DependencyGraphProof

                                    ↳ QDP

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ DependencyGraphProof

                                            ↳ QDP

                                              ↳ Narrowing

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                    ↳ QDP

                                                      ↳ Narrowing

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ QDP

                                                              ↳ QDPOrderProof

                                                                ↳ QDP

                                                                  ↳ QDPOrderProof

                                                                    ↳ QDP

                                                                      ↳ QDPOrderProof

                                                                        ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(add(add(x0, x1), y1)) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(add(fact(x0), y1)) → ADDACTIVE(factActive(mark(x0)), mark(y1))
MARK(if(add(x0, x1), y1, y2)) → IFACTIVE(addActive(mark(x0), mark(x1)), y1, y2)
MARK(add(s(x0), y1)) → ADDACTIVE(s(mark(x0)), mark(y1))
MARK(prod(s(x0), y1)) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(if(fact(x0), y1, y2)) → IFACTIVE(factActive(mark(x0)), y1, y2)
MARK(if(x1, x2, x3)) → MARK(x1)
MARK(if(true, y1, y2)) → IFACTIVE(true, y1, y2)
PRODACTIVE(s(s(x0)), y1) → PRODACTIVE(s(mark(x0)), mark(y1))
MARK(p(x1)) → MARK(x1)
MARK(add(prod(x0, x1), y1)) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(prod(x0, x1)), y1) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
PRODACTIVE(s(fact(x0)), y1) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(p(p(x0))) → PACTIVE(pActive(mark(x0)))
MARK(if(if(x0, x1, x2), y1, y2)) → IFACTIVE(ifActive(mark(x0), x1, x2), y1, y2)
MARK(prod(add(x0, x1), y1)) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(if(zero(x0), y1, y2)) → IFACTIVE(zeroActive(mark(x0)), y1, y2)
MARK(p(add(x0, x1))) → PACTIVE(addActive(mark(x0), mark(x1)))
MARK(if(p(x0), y1, y2)) → IFACTIVE(pActive(mark(x0)), y1, y2)
ADDACTIVE(s(0), y1) → ADDACTIVE(0, mark(y1))
ADDACTIVE(s(if(x0, x1, x2)), y1) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
PRODACTIVE(s(X), Y) → ADDACTIVE(mark(Y), prodActive(mark(X), mark(Y)))
ADDACTIVE(s(p(x0)), y1) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PRODACTIVE(s(add(x0, x1)), y1) → PRODACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(p(prod(x0, x1))) → PACTIVE(prodActive(mark(x0), mark(x1)))
MARK(p(fact(x0))) → PACTIVE(factActive(mark(x0)))
ADDACTIVE(s(s(x0)), y1) → ADDACTIVE(s(mark(x0)), mark(y1))
ADDACTIVE(s(X), Y) → MARK(X)
MARK(zero(x1)) → MARK(x1)
PRODACTIVE(s(X), Y) → MARK(Y)
MARK(prod(x1, x2)) → MARK(x1)
MARK(s(x1)) → MARK(x1)
MARK(add(x1, x2)) → MARK(x2)
MARK(p(s(x0))) → PACTIVE(s(mark(x0)))
MARK(fact(x1)) → MARK(x1)
ADDACTIVE(0, X) → MARK(X)
MARK(add(x1, x2)) → MARK(x1)
IFACTIVE(true, X, Y) → MARK(X)
FACTACTIVE(X) → IFACTIVE(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
PRODACTIVE(s(p(x0)), y1) → PRODACTIVE(pActive(mark(x0)), mark(y1))
ADDACTIVE(s(prod(x0, x1)), y1) → ADDACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(fact(x1)) → FACTACTIVE(mark(x1))
MARK(prod(prod(x0, x1), y1)) → PRODACTIVE(prodActive(mark(x0), mark(x1)), mark(y1))
MARK(if(prod(x0, x1), y1, y2)) → IFACTIVE(prodActive(mark(x0), mark(x1)), y1, y2)
MARK(p(if(x0, x1, x2))) → PACTIVE(ifActive(mark(x0), x1, x2))
MARK(add(p(x0), y1)) → ADDACTIVE(pActive(mark(x0)), mark(y1))
PACTIVE(s(X)) → MARK(X)
IFACTIVE(false, X, Y) → MARK(Y)
MARK(add(0, y1)) → ADDACTIVE(0, mark(y1))
MARK(prod(x1, x2)) → MARK(x2)
ADDACTIVE(s(fact(x0)), y1) → ADDACTIVE(factActive(mark(x0)), mark(y1))
PRODACTIVE(s(X), Y) → MARK(X)
PRODACTIVE(s(if(x0, x1, x2)), y1) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(X), Y) → MARK(Y)
FACTACTIVE(X) → MARK(X)
MARK(if(false, y1, y2)) → IFACTIVE(false, y1, y2)
MARK(add(if(x0, x1, x2), y1)) → ADDACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
MARK(prod(if(x0, x1, x2), y1)) → PRODACTIVE(ifActive(mark(x0), x1, x2), mark(y1))
ADDACTIVE(s(add(x0, x1)), y1) → ADDACTIVE(addActive(mark(x0), mark(x1)), mark(y1))
MARK(prod(fact(x0), y1)) → PRODACTIVE(factActive(mark(x0)), mark(y1))
MARK(prod(p(x0), y1)) → PRODACTIVE(pActive(mark(x0)), mark(y1))

The TRS R consists of the following rules:

mark(fact(x1)) → factActive(mark(x1))
factActive(x1) → fact(x1)
mark(add(x1, x2)) → addActive(mark(x1), mark(x2))
addActive(x1, x2) → add(x1, x2)
mark(prod(x1, x2)) → prodActive(mark(x1), mark(x2))
prodActive(x1, x2) → prod(x1, x2)
mark(if(x1, x2, x3)) → ifActive(mark(x1), x2, x3)
ifActive(x1, x2, x3) → if(x1, x2, x3)
mark(zero(x1)) → zeroActive(mark(x1))
zeroActive(x1) → zero(x1)
mark(p(x1)) → pActive(mark(x1))
pActive(x1) → p(x1)
mark(s(x1)) → s(mark(x1))
mark(0) → 0
mark(true) → true
mark(false) → false
factActive(X) → ifActive(zeroActive(mark(X)), s(0), prod(X, fact(p(X))))
addActive(0, X) → mark(X)
addActive(s(X), Y) → s(addActive(mark(X), mark(Y)))
prodActive(0, X) → 0
prodActive(s(X), Y) → addActive(mark(Y), prodActive(mark(X), mark(Y)))
ifActive(true, X, Y) → mark(X)
ifActive(false, X, Y) → mark(Y)
zeroActive(0) → true
zeroActive(s(X)) → false
pActive(s(X)) → mark(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Trivial transformation to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

FACT(X) → PROD(X, fact(p(X)))
PROD(s(X), Y) → ADD(Y, prod(X, Y))
FACT(X) → P(X)
ADD(s(X), Y) → ADD(X, Y)
FACT(X) → FACT(p(X))
PROD(s(X), Y) → PROD(X, Y)
FACT(X) → ZERO(X)
FACT(X) → IF(zero(X), s(0), prod(X, fact(p(X))))

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

FACT(X) → PROD(X, fact(p(X)))
PROD(s(X), Y) → ADD(Y, prod(X, Y))
FACT(X) → P(X)
ADD(s(X), Y) → ADD(X, Y)
FACT(X) → FACT(p(X))
PROD(s(X), Y) → PROD(X, Y)
FACT(X) → ZERO(X)
FACT(X) → IF(zero(X), s(0), prod(X, fact(p(X))))

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 3 SCCs with 5 less nodes.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ UsableRulesProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ADD(s(X), Y) → ADD(X, Y)

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ADD(s(X), Y) → ADD(X, Y)

R is empty.
The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ADD(s(X), Y) → ADD(X, Y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ADD(s(X), Y) → ADD(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROD(s(X), Y) → PROD(X, Y)

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROD(s(X), Y) → PROD(X, Y)

R is empty.
The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PROD(s(X), Y) → PROD(X, Y)

From the DPs we obtained the following set of size-change graphs:

PROD(s(X), Y) → PROD(X, Y)
The graph contains the following edges 1 > 1, 2 >= 2

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

FACT(X) → FACT(p(X))

The TRS R consists of the following rules:

fact(X) → if(zero(X), s(0), prod(X, fact(p(X))))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
prod(0, X) → 0
prod(s(X), Y) → add(Y, prod(X, Y))
if(true, X, Y) → X
if(false, X, Y) → Y
zero(0) → true
zero(s(X)) → false
p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

FACT(X) → FACT(p(X))

The TRS R consists of the following rules:

p(s(X)) → X

The set Q consists of the following terms:

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))
p(s(x0))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

fact(x0)
add(0, x0)
add(s(x0), x1)
prod(0, x0)
prod(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
zero(0)
zero(s(x0))

↳ CSR

  ↳ CSRInnermostProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ Overlay + Local Confluence

        ↳ QTRS

          ↳ DependencyPairsProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ UsableRulesProof

                      ↳ QDP

                        ↳ QReductionProof

                          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FACT(X) → FACT(p(X))

The TRS R consists of the following rules:

p(s(X)) → X

The set Q consists of the following terms:

p(s(x0))

We have to consider all minimal (P,Q,R)-chains.